A, B:Realizer.
R-Feasible(A)
 R-Feasible(B)
 (i:Id.
 ((j:Id. R-has-loc(A;j) = i = j  )
 (& kdom(R-da(A;i)). 

 (& T=R-da(A;i)(k)  
 (& Tisrcv(k)
 (& T (source(lnk(k)) = i  Id  T  R-da(B;destination(lnk(k)))(k)?Top)
 (& T & (destination(lnk(k)) = i  Id  R-da(B;source(lnk(k)))(k)?Void  T))
 R-icompat(A;B) 

latex

Definitions	R-interface(A;B), x:A. B(x), t  T, P  Q, x:A. B(x), Realizer, R-Feasible(R), Knd, Top, x. t(x), a:A fp B(a), Type, x.A(x), R-da(R;i), x:AB(x), KindDeq, f(x), Void, lnk(k), source(l), f(x)?z, destination(l), Id, s = t, x:AB(x), P & Q, isrcv(k), b, x  dom(f), a = b, R-has-loc(R;i), , R-icompat(A;B), xdom(f). v=f(x)   P(x;v), Prop, P  Q, True, T, P  Q, {T}, SQType(T), s ~ t, Atom$n
Lemmas	R-interface-iff2, Id sq, R-interface-iff, squash wf, true wf, assert-eq-id, bool wf, R-has-loc wf, eq id wf, fpf-dom wf, assert wf, isrcv wf, Id wf, ldst wf, fpf-cap wf, lsrc wf, lnk wf, fpf-ap wf, Kind-deq wf, fpf-trivial-subtype-top, R-da wf, fpf wf, top wf, Knd wf, R-Feasible wf, es realizer wf, R-interface-icompat